package com.graphcoloring;

import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ISolver;

import java.util.List;
import java.util.Set;


public class StandardBitwiseSolver implements Solver {
    public Solution solve(GraphInputData inputData) throws Exception {
        int n = inputData.getVertexNumber();
        List<Integer[]> edges = inputData.getEdgeList();

        int colorsCount = n;
        int colors[] = new int[n];

        for (int k = n; k >= 1; k--) {

            if (k == 1) {
                Solution solution = new Solution();
                solution.colorCount = colorsCount;
                solution.colors = colors;
                return solution;
            }
            int l = (int) Math.ceil((Math.log(k) / Math.log(2)));

            ISolver solver = SolverFactory.newDefault();
            solver.setTimeout(60);
            solver.newVar(n * l + 1);

            for (Integer[] edge : edges) {
                int vertex1 = edge[0];
                int vertex2 = edge[1];

                int[] xvars = new int[l];      // names of the variables corresponding to bits of vertex 1
                int[] yvars = new int[l];

                for (int i = 0; i < l; ++i) {
                    xvars[i] = (vertex1 * l + i) + 1;
                    yvars[i] = (vertex2 * l + i) + 1;
                }

                for (int i = 0; i < Math.pow(2, l); ++i) {
                    int[] clause = new int[2 * l];
                    int j = i;

                    int[] bits = new int[l];
                    int pos = 0;
                    while (j != 0) {
                        bits[pos] = j % 2;
                        j = j / 2;
                        pos++;
                    }
                    for (int b = 0; b < l; ++b) {

                        if (bits[b] == 1) {
                            clause[b * 2] = xvars[b];
                            clause[b * 2 + 1] = yvars[b];
                        } else {
                            clause[b * 2] = -xvars[b];
                            clause[b * 2 + 1] = -yvars[b];
                        }
                    }
                    solver.addClause(new VecInt(clause));
                }
            }
            Set<Integer> vertices = inputData.getConnectedEdges().keySet();

            for (int vertice : vertices) {
                for (int i = k; i < Math.pow(2, l); i++) {
                    int[] clause = new int[l];
                    int var = vertice;
                    int j = i;

                    int[] bits = new int[l];
                    int pos = 0;
                    while (j != 0) {
                        bits[pos] = j % 2;
                        j = j / 2;
                        pos++;
                    }
                    for (int b = 0; b < l; b++) {
                        if (bits[b] == 0) {
                            clause[b] = (var * l + b + 1);
                        } else {
                            clause[b] = -(var * l + b + 1);
                        }
                    }
                    solver.addClause(new VecInt(clause));
                }
            }


            if (solver.isSatisfiable()) {
                int model[] = solver.model();
                colorsCount = k;
                for (int vertex = 0; vertex < n; ++vertex) {
                    int color = 0, mult = 1;
                    for (int bit = 1; bit <= l; ++bit) {
                        if (model[vertex * l + bit -1] > 0) color += mult;
                        mult *= 2;
                    }
                    colors[vertex] = color;
                }
            } else {
                Solution solution = new Solution();
                solution.colorCount = colorsCount;
                solution.colors = colors;
                return solution;
            }

        }
        return null;
    }
}